$\forall$$T$:Type, $a$, $b$:($T$ List).
\\[0ex]($\parallel$$a$$\parallel$ = $\parallel$$b$$\parallel$ $\in$ $\mathbb{Z}$) $\Rightarrow$ ($\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$$a$$\parallel$) $\Rightarrow$ ($a$[$i$] = $b$[$i$] $\in$ $T$)) $\Rightarrow$ ($a$ = $b$)